<!DOCTYPE html PUBLIC "-//W3C//DTD XHTML 1.0 Strict//EN"
"http://www.w3.org/TR/xhtml1/DTD/xhtml1-strict.dtd">
<html xmlns="http://www.w3.org/1999/xhtml">
<head>
<meta http-equiv="Content-Type" content="text/html; charset=utf-8"/>
<link href="common/css/sf.css" rel="stylesheet" type="text/css"/>
<title>Types: 类型系统</title>
</head>
<link href="common/jquery-ui/jquery-ui.css" rel="stylesheet">
<script src="common/jquery-ui/external/jquery/jquery.js"></script>
<script src="common/jquery-ui/jquery-ui.js"></script>
<script src="common/toggleproofs.js"></script>
<link href="common/css/plf.css" rel="stylesheet" type="text/css"/>

<body>

<div id="page">

<div id="header">
<a href='https://coq-zh.github.io/SF-zh/index.html'>
<img src='common/media/image/sf_logo_sm.png'></a>
</br><a href='index.html'>  <span class='booktitleinheader'>Volume 2: 编程语言基础</span><br></br>
<ul id='menu'>
   <a href='toc.html'><li class='section_name'>目录</li></a>
   <a href='coqindex.html'><li class='section_name'>索引</li></a>
   <a href='deps.html'><li class='section_name'>路线</li></a>
</ul>
</a></div>

<div id="main">

<h1 class="libtitle">Types<span class="subtitle">类型系统</span></h1>


<div class="doc">

<div class="paragraph"> </div>

 我们接下来主要的话题是<b>类型系统</b>——一种根据表达式结果的“形状（shapes）”
    来给表达式分类的静态程序分析技术。我们将会以一个最简单的有类型语言为起点，介绍
    类型和定型规则的概念，以及类型系统最基础的几个定理：<b>保型性（type preservation）</b>
    和<b>可进性（progress）</b>。在 <a href="Stlc.html"><span class="inlineref">Stlc</span></a> 一章中，我们会继续考察
    <b>简单类型λ-演算</b>，它是几乎每个现代函数式语言的核心（也包括 Coq！）。 
</div>
<div class="code code-tight">

<span class="id" type="keyword">Set</span> <span class="id" type="var">Warnings</span> "-notation-overridden,-parsing".<br/>
<span class="id" type="var">From</span> <span class="id" type="var">Coq</span> <span class="id" type="keyword">Require</span> <span class="id" type="keyword">Import</span> <span class="id" type="var">Arith.Arith</span>.<br/>
<span class="id" type="var">From</span> <span class="id" type="var">PLF</span> <span class="id" type="keyword">Require</span> <span class="id" type="keyword">Import</span> <span class="id" type="var">Maps</span>.<br/>
<span class="id" type="var">From</span> <span class="id" type="var">PLF</span> <span class="id" type="keyword">Require</span> <span class="id" type="keyword">Import</span> <span class="id" type="var">Imp</span>.<br/>
<span class="id" type="var">From</span> <span class="id" type="var">PLF</span> <span class="id" type="keyword">Require</span> <span class="id" type="keyword">Import</span> <span class="id" type="var">Smallstep</span>.<br/><hr class='doublespaceincode'/>
<span class="id" type="keyword">Hint</span> <span class="id" type="var">Constructors</span> <span class="id" type="var">multi</span>.<br/>
</div>

<div class="doc">
<a name="lab174"></a><h1 class="section">有类型算数表达式</h1>

<div class="paragraph"> </div>

 作为对类型系统讨论的动机，让我们像过去一样以一个小型玩具语言开始。
    我们想要让程序有机会产生运行时类型错误，因此除了 <a href="Smallstep.html"><span class="inlineref">Smallstep</span></a>
    一章中用到的常量和加法，还需要一点更复杂的语言构造：只有一种数据类型（比如说数字）
    太过于简单，但是两种（数字和布尔值）便足够产生有趣的故事了。

<div class="paragraph"> </div>

    语言的定义部分没有什么特别值得注意的。 
</div>

<div class="doc">
<a name="lab175"></a><h2 class="section">语法</h2>

<div class="paragraph"> </div>

 这是非形式化的语法表述：

<div class="paragraph"> </div>

<div class="code code-tight">
&nbsp;&nbsp;&nbsp;&nbsp;<span class="id" type="var">t</span>&nbsp;<span style='font-size:85%;'><span style='vertical-align:5%;'><span style='letter-spacing:-.2em;'>:</span>:</span>=</span>&nbsp;<span class="id" type="var">tru</span><br/>
&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;|&nbsp;<span class="id" type="var">fls</span><br/>
&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;|&nbsp;<span class="id" type="var">test</span>&nbsp;<span class="id" type="var">t</span>&nbsp;<span class="id" type="keyword">then</span>&nbsp;<span class="id" type="var">t</span>&nbsp;<span class="id" type="keyword">else</span>&nbsp;<span class="id" type="var">t</span><br/>
&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;|&nbsp;<span class="id" type="var">zro</span><br/>
&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;|&nbsp;<span class="id" type="var">scc</span>&nbsp;<span class="id" type="var">t</span><br/>
&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;|&nbsp;<span class="id" type="var">prd</span>&nbsp;<span class="id" type="var">t</span><br/>
&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;|&nbsp;<span class="id" type="var">iszro</span>&nbsp;<span class="id" type="var">t</span>
<div class="paragraph"> </div>

</div>
    以及形式化的： 
</div>
<div class="code code-tight">

<span class="id" type="keyword">Inductive</span> <span class="id" type="var">tm</span> : <span class="id" type="keyword">Type</span> :=<br/>
&nbsp;&nbsp;| <span class="id" type="var">tru</span> : <span class="id" type="var">tm</span><br/>
&nbsp;&nbsp;| <span class="id" type="var">fls</span> : <span class="id" type="var">tm</span><br/>
&nbsp;&nbsp;| <span class="id" type="var">test</span> : <span class="id" type="var">tm</span> → <span class="id" type="var">tm</span> → <span class="id" type="var">tm</span> → <span class="id" type="var">tm</span><br/>
&nbsp;&nbsp;| <span class="id" type="var">zro</span> : <span class="id" type="var">tm</span><br/>
&nbsp;&nbsp;| <span class="id" type="var">scc</span> : <span class="id" type="var">tm</span> → <span class="id" type="var">tm</span><br/>
&nbsp;&nbsp;| <span class="id" type="var">prd</span> : <span class="id" type="var">tm</span> → <span class="id" type="var">tm</span><br/>
&nbsp;&nbsp;| <span class="id" type="var">iszro</span> : <span class="id" type="var">tm</span> → <span class="id" type="var">tm</span>.<br/>
</div>

<div class="doc">
对<b>值（values）</b>的定义包括 <span class="inlinecode"><span class="id" type="var">tru</span></span>，<span class="inlinecode"><span class="id" type="var">fls</span></span> 以及数值…… 
</div>
<div class="code code-tight">

<span class="id" type="keyword">Inductive</span> <span class="id" type="var">bvalue</span> : <span class="id" type="var">tm</span> → <span class="id" type="keyword">Prop</span> :=<br/>
&nbsp;&nbsp;| <span class="id" type="var">bv_tru</span> : <span class="id" type="var">bvalue</span> <span class="id" type="var">tru</span><br/>
&nbsp;&nbsp;| <span class="id" type="var">bv_fls</span> : <span class="id" type="var">bvalue</span> <span class="id" type="var">fls</span>.<br/><hr class='doublespaceincode'/>
<span class="id" type="keyword">Inductive</span> <span class="id" type="var">nvalue</span> : <span class="id" type="var">tm</span> → <span class="id" type="keyword">Prop</span> :=<br/>
&nbsp;&nbsp;| <span class="id" type="var">nv_zro</span> : <span class="id" type="var">nvalue</span> <span class="id" type="var">zro</span><br/>
&nbsp;&nbsp;| <span class="id" type="var">nv_scc</span> : <span style='font-size:120%;'>&forall;</span><span class="id" type="var">t</span>, <span class="id" type="var">nvalue</span> <span class="id" type="var">t</span> → <span class="id" type="var">nvalue</span> (<span class="id" type="var">scc</span> <span class="id" type="var">t</span>).<br/><hr class='doublespaceincode'/>
<span class="id" type="keyword">Definition</span> <span class="id" type="var">value</span> (<span class="id" type="var">t</span> : <span class="id" type="var">tm</span>) := <span class="id" type="var">bvalue</span> <span class="id" type="var">t</span> ∨ <span class="id" type="var">nvalue</span> <span class="id" type="var">t</span>.<br/><hr class='doublespaceincode'/>
<span class="id" type="keyword">Hint</span> <span class="id" type="var">Constructors</span> <span class="id" type="var">bvalue</span> <span class="id" type="var">nvalue</span>.<br/>
<span class="id" type="keyword">Hint</span> <span class="id" type="keyword">Unfold</span> <span class="id" type="var">value</span>.<br/>
<span class="id" type="keyword">Hint</span> <span class="id" type="keyword">Unfold</span> <span class="id" type="var">update</span>.<br/>
</div>

<div class="doc">
<a name="lab176"></a><h2 class="section">操作语义</h2>

<div class="paragraph"> </div>

 首先我们非形式化地描述单步关系…… 
<div class="paragraph"> </div>

<center><table class="infrule">
<tr class="infruleassumption">
  <td class="infrule">&nbsp;&nbsp;</td>
  <td class="infrulenamecol" rowspan="3">
    (ST_TestTru) &nbsp;
  </td></tr>
<tr class="infrulemiddle">
  <td class="infrule"><hr /></td>
</tr>
<tr class="infruleassumption">
  <td class="infrule">test&nbsp;tru&nbsp;then&nbsp;t<sub>1</sub>&nbsp;else&nbsp;t<sub>2</sub>&nbsp;<span class="nowrap"><span style='font-size:85%;'><span style='vertical-align:6%;'><span style='letter-spacing:-.2em;'>-</span><span style='letter-spacing:-.2em;'>-</span></span>&gt;</span></span>&nbsp;t<sub>1</sub></td>
  <td></td>
</td>
</table></center><center><table class="infrule">
<tr class="infruleassumption">
  <td class="infrule">&nbsp;&nbsp;</td>
  <td class="infrulenamecol" rowspan="3">
    (ST_TestFls) &nbsp;
  </td></tr>
<tr class="infrulemiddle">
  <td class="infrule"><hr /></td>
</tr>
<tr class="infruleassumption">
  <td class="infrule">test&nbsp;fls&nbsp;then&nbsp;t<sub>1</sub>&nbsp;else&nbsp;t<sub>2</sub>&nbsp;<span class="nowrap"><span style='font-size:85%;'><span style='vertical-align:6%;'><span style='letter-spacing:-.2em;'>-</span><span style='letter-spacing:-.2em;'>-</span></span>&gt;</span></span>&nbsp;t<sub>2</sub></td>
  <td></td>
</td>
</table></center><center><table class="infrule">
<tr class="infruleassumption">
  <td class="infrule">t<sub>1</sub>&nbsp;<span class="nowrap"><span style='font-size:85%;'><span style='vertical-align:6%;'><span style='letter-spacing:-.2em;'>-</span><span style='letter-spacing:-.2em;'>-</span></span>&gt;</span></span>&nbsp;t<sub>1</sub>'</td>
  <td class="infrulenamecol" rowspan="3">
    (ST_Test) &nbsp;
  </td></tr>
<tr class="infrulemiddle">
  <td class="infrule"><hr /></td>
</tr>
<tr class="infruleassumption">
  <td class="infrule">test&nbsp;t<sub>1</sub>&nbsp;then&nbsp;t<sub>2</sub>&nbsp;else&nbsp;t<sub>3</sub>&nbsp;<span class="nowrap"><span style='font-size:85%;'><span style='vertical-align:6%;'><span style='letter-spacing:-.2em;'>-</span><span style='letter-spacing:-.2em;'>-</span></span>&gt;</span></span>&nbsp;test&nbsp;t<sub>1</sub>'&nbsp;then&nbsp;t<sub>2</sub>&nbsp;else&nbsp;t<sub>3</sub></td>
  <td></td>
</td>
</table></center><center><table class="infrule">
<tr class="infruleassumption">
  <td class="infrule">t<sub>1</sub>&nbsp;<span class="nowrap"><span style='font-size:85%;'><span style='vertical-align:6%;'><span style='letter-spacing:-.2em;'>-</span><span style='letter-spacing:-.2em;'>-</span></span>&gt;</span></span>&nbsp;t<sub>1</sub>'</td>
  <td class="infrulenamecol" rowspan="3">
    (ST_Scc) &nbsp;
  </td></tr>
<tr class="infrulemiddle">
  <td class="infrule"><hr /></td>
</tr>
<tr class="infruleassumption">
  <td class="infrule">scc&nbsp;t<sub>1</sub>&nbsp;<span class="nowrap"><span style='font-size:85%;'><span style='vertical-align:6%;'><span style='letter-spacing:-.2em;'>-</span><span style='letter-spacing:-.2em;'>-</span></span>&gt;</span></span>&nbsp;scc&nbsp;t<sub>1</sub>'</td>
  <td></td>
</td>
</table></center><center><table class="infrule">
<tr class="infruleassumption">
  <td class="infrule">&nbsp;&nbsp;</td>
  <td class="infrulenamecol" rowspan="3">
    (ST_PrdZro) &nbsp;
  </td></tr>
<tr class="infrulemiddle">
  <td class="infrule"><hr /></td>
</tr>
<tr class="infruleassumption">
  <td class="infrule">prd&nbsp;zro&nbsp;<span class="nowrap"><span style='font-size:85%;'><span style='vertical-align:6%;'><span style='letter-spacing:-.2em;'>-</span><span style='letter-spacing:-.2em;'>-</span></span>&gt;</span></span>&nbsp;zro</td>
  <td></td>
</td>
</table></center><center><table class="infrule">
<tr class="infruleassumption">
  <td class="infrule">numeric&nbsp;value&nbsp;v<sub>1</sub></td>
  <td class="infrulenamecol" rowspan="3">
    (ST_PrdScc) &nbsp;
  </td></tr>
<tr class="infrulemiddle">
  <td class="infrule"><hr /></td>
</tr>
<tr class="infruleassumption">
  <td class="infrule">prd&nbsp;(scc&nbsp;v<sub>1</sub>)&nbsp;<span class="nowrap"><span style='font-size:85%;'><span style='vertical-align:6%;'><span style='letter-spacing:-.2em;'>-</span><span style='letter-spacing:-.2em;'>-</span></span>&gt;</span></span>&nbsp;v<sub>1</sub></td>
  <td></td>
</td>
</table></center><center><table class="infrule">
<tr class="infruleassumption">
  <td class="infrule">t<sub>1</sub>&nbsp;<span class="nowrap"><span style='font-size:85%;'><span style='vertical-align:6%;'><span style='letter-spacing:-.2em;'>-</span><span style='letter-spacing:-.2em;'>-</span></span>&gt;</span></span>&nbsp;t<sub>1</sub>'</td>
  <td class="infrulenamecol" rowspan="3">
    (ST_Prd) &nbsp;
  </td></tr>
<tr class="infrulemiddle">
  <td class="infrule"><hr /></td>
</tr>
<tr class="infruleassumption">
  <td class="infrule">prd&nbsp;t<sub>1</sub>&nbsp;<span class="nowrap"><span style='font-size:85%;'><span style='vertical-align:6%;'><span style='letter-spacing:-.2em;'>-</span><span style='letter-spacing:-.2em;'>-</span></span>&gt;</span></span>&nbsp;prd&nbsp;t<sub>1</sub>'</td>
  <td></td>
</td>
</table></center><center><table class="infrule">
<tr class="infruleassumption">
  <td class="infrule">&nbsp;&nbsp;</td>
  <td class="infrulenamecol" rowspan="3">
    (ST_IszroZro) &nbsp;
  </td></tr>
<tr class="infrulemiddle">
  <td class="infrule"><hr /></td>
</tr>
<tr class="infruleassumption">
  <td class="infrule">iszro&nbsp;zro&nbsp;<span class="nowrap"><span style='font-size:85%;'><span style='vertical-align:6%;'><span style='letter-spacing:-.2em;'>-</span><span style='letter-spacing:-.2em;'>-</span></span>&gt;</span></span>&nbsp;tru</td>
  <td></td>
</td>
</table></center><center><table class="infrule">
<tr class="infruleassumption">
  <td class="infrule">numeric&nbsp;value&nbsp;v<sub>1</sub></td>
  <td class="infrulenamecol" rowspan="3">
    (ST_IszroScc) &nbsp;
  </td></tr>
<tr class="infrulemiddle">
  <td class="infrule"><hr /></td>
</tr>
<tr class="infruleassumption">
  <td class="infrule">iszro&nbsp;(scc&nbsp;v<sub>1</sub>)&nbsp;<span class="nowrap"><span style='font-size:85%;'><span style='vertical-align:6%;'><span style='letter-spacing:-.2em;'>-</span><span style='letter-spacing:-.2em;'>-</span></span>&gt;</span></span>&nbsp;fls</td>
  <td></td>
</td>
</table></center><center><table class="infrule">
<tr class="infruleassumption">
  <td class="infrule">t<sub>1</sub>&nbsp;<span class="nowrap"><span style='font-size:85%;'><span style='vertical-align:6%;'><span style='letter-spacing:-.2em;'>-</span><span style='letter-spacing:-.2em;'>-</span></span>&gt;</span></span>&nbsp;t<sub>1</sub>'</td>
  <td class="infrulenamecol" rowspan="3">
    (ST_Iszro) &nbsp;
  </td></tr>
<tr class="infrulemiddle">
  <td class="infrule"><hr /></td>
</tr>
<tr class="infruleassumption">
  <td class="infrule">iszro&nbsp;t<sub>1</sub>&nbsp;<span class="nowrap"><span style='font-size:85%;'><span style='vertical-align:6%;'><span style='letter-spacing:-.2em;'>-</span><span style='letter-spacing:-.2em;'>-</span></span>&gt;</span></span>&nbsp;iszro&nbsp;t<sub>1</sub>'</td>
  <td></td>
</td>
</table></center>
<div class="paragraph"> </div>

 接着形式化地： 
</div>
<div class="code code-tight">

<span class="id" type="keyword">Reserved Notation</span> "t<sub>1</sub> '<span class="nowrap"><span style='font-size:85%;'><span style='vertical-align:6%;'><span style='letter-spacing:-.2em;'>-</span><span style='letter-spacing:-.2em;'>-</span></span>&gt;</span></span>' t<sub>2</sub>" (<span class="id" type="tactic">at</span> <span class="id" type="var">level</span> 40).<br/><hr class='doublespaceincode'/>
<span class="id" type="keyword">Inductive</span> <span class="id" type="var">step</span> : <span class="id" type="var">tm</span> → <span class="id" type="var">tm</span> → <span class="id" type="keyword">Prop</span> :=<br/>
&nbsp;&nbsp;| <span class="id" type="var">ST_TestTru</span> : <span style='font-size:120%;'>&forall;</span><span class="id" type="var">t<sub>1</sub></span> <span class="id" type="var">t<sub>2</sub></span>,<br/>
&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;(<span class="id" type="var">test</span> <span class="id" type="var">tru</span> <span class="id" type="var">t<sub>1</sub></span> <span class="id" type="var">t<sub>2</sub></span>) <span class="nowrap"><span style='font-size:85%;'><span style='vertical-align:6%;'><span style='letter-spacing:-.2em;'>-</span><span style='letter-spacing:-.2em;'>-</span></span>&gt;</span></span> <span class="id" type="var">t<sub>1</sub></span><br/>
&nbsp;&nbsp;| <span class="id" type="var">ST_TestFls</span> : <span style='font-size:120%;'>&forall;</span><span class="id" type="var">t<sub>1</sub></span> <span class="id" type="var">t<sub>2</sub></span>,<br/>
&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;(<span class="id" type="var">test</span> <span class="id" type="var">fls</span> <span class="id" type="var">t<sub>1</sub></span> <span class="id" type="var">t<sub>2</sub></span>) <span class="nowrap"><span style='font-size:85%;'><span style='vertical-align:6%;'><span style='letter-spacing:-.2em;'>-</span><span style='letter-spacing:-.2em;'>-</span></span>&gt;</span></span> <span class="id" type="var">t<sub>2</sub></span><br/>
&nbsp;&nbsp;| <span class="id" type="var">ST_Test</span> : <span style='font-size:120%;'>&forall;</span><span class="id" type="var">t<sub>1</sub></span> <span class="id" type="var">t<sub>1</sub>'</span> <span class="id" type="var">t<sub>2</sub></span> <span class="id" type="var">t<sub>3</sub></span>,<br/>
&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;<span class="id" type="var">t<sub>1</sub></span> <span class="nowrap"><span style='font-size:85%;'><span style='vertical-align:6%;'><span style='letter-spacing:-.2em;'>-</span><span style='letter-spacing:-.2em;'>-</span></span>&gt;</span></span> <span class="id" type="var">t<sub>1</sub>'</span> →<br/>
&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;(<span class="id" type="var">test</span> <span class="id" type="var">t<sub>1</sub></span> <span class="id" type="var">t<sub>2</sub></span> <span class="id" type="var">t<sub>3</sub></span>) <span class="nowrap"><span style='font-size:85%;'><span style='vertical-align:6%;'><span style='letter-spacing:-.2em;'>-</span><span style='letter-spacing:-.2em;'>-</span></span>&gt;</span></span> (<span class="id" type="var">test</span> <span class="id" type="var">t<sub>1</sub>'</span> <span class="id" type="var">t<sub>2</sub></span> <span class="id" type="var">t<sub>3</sub></span>)<br/>
&nbsp;&nbsp;| <span class="id" type="var">ST_Scc</span> : <span style='font-size:120%;'>&forall;</span><span class="id" type="var">t<sub>1</sub></span> <span class="id" type="var">t<sub>1</sub>'</span>,<br/>
&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;<span class="id" type="var">t<sub>1</sub></span> <span class="nowrap"><span style='font-size:85%;'><span style='vertical-align:6%;'><span style='letter-spacing:-.2em;'>-</span><span style='letter-spacing:-.2em;'>-</span></span>&gt;</span></span> <span class="id" type="var">t<sub>1</sub>'</span> →<br/>
&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;(<span class="id" type="var">scc</span> <span class="id" type="var">t<sub>1</sub></span>) <span class="nowrap"><span style='font-size:85%;'><span style='vertical-align:6%;'><span style='letter-spacing:-.2em;'>-</span><span style='letter-spacing:-.2em;'>-</span></span>&gt;</span></span> (<span class="id" type="var">scc</span> <span class="id" type="var">t<sub>1</sub>'</span>)<br/>
&nbsp;&nbsp;| <span class="id" type="var">ST_PrdZro</span> :<br/>
&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;(<span class="id" type="var">prd</span> <span class="id" type="var">zro</span>) <span class="nowrap"><span style='font-size:85%;'><span style='vertical-align:6%;'><span style='letter-spacing:-.2em;'>-</span><span style='letter-spacing:-.2em;'>-</span></span>&gt;</span></span> <span class="id" type="var">zro</span><br/>
&nbsp;&nbsp;| <span class="id" type="var">ST_PrdScc</span> : <span style='font-size:120%;'>&forall;</span><span class="id" type="var">t<sub>1</sub></span>,<br/>
&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;<span class="id" type="var">nvalue</span> <span class="id" type="var">t<sub>1</sub></span> →<br/>
&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;(<span class="id" type="var">prd</span> (<span class="id" type="var">scc</span> <span class="id" type="var">t<sub>1</sub></span>)) <span class="nowrap"><span style='font-size:85%;'><span style='vertical-align:6%;'><span style='letter-spacing:-.2em;'>-</span><span style='letter-spacing:-.2em;'>-</span></span>&gt;</span></span> <span class="id" type="var">t<sub>1</sub></span><br/>
&nbsp;&nbsp;| <span class="id" type="var">ST_Prd</span> : <span style='font-size:120%;'>&forall;</span><span class="id" type="var">t<sub>1</sub></span> <span class="id" type="var">t<sub>1</sub>'</span>,<br/>
&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;<span class="id" type="var">t<sub>1</sub></span> <span class="nowrap"><span style='font-size:85%;'><span style='vertical-align:6%;'><span style='letter-spacing:-.2em;'>-</span><span style='letter-spacing:-.2em;'>-</span></span>&gt;</span></span> <span class="id" type="var">t<sub>1</sub>'</span> →<br/>
&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;(<span class="id" type="var">prd</span> <span class="id" type="var">t<sub>1</sub></span>) <span class="nowrap"><span style='font-size:85%;'><span style='vertical-align:6%;'><span style='letter-spacing:-.2em;'>-</span><span style='letter-spacing:-.2em;'>-</span></span>&gt;</span></span> (<span class="id" type="var">prd</span> <span class="id" type="var">t<sub>1</sub>'</span>)<br/>
&nbsp;&nbsp;| <span class="id" type="var">ST_IszroZro</span> :<br/>
&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;(<span class="id" type="var">iszro</span> <span class="id" type="var">zro</span>) <span class="nowrap"><span style='font-size:85%;'><span style='vertical-align:6%;'><span style='letter-spacing:-.2em;'>-</span><span style='letter-spacing:-.2em;'>-</span></span>&gt;</span></span> <span class="id" type="var">tru</span><br/>
&nbsp;&nbsp;| <span class="id" type="var">ST_IszroScc</span> : <span style='font-size:120%;'>&forall;</span><span class="id" type="var">t<sub>1</sub></span>,<br/>
&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;<span class="id" type="var">nvalue</span> <span class="id" type="var">t<sub>1</sub></span> →<br/>
&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;(<span class="id" type="var">iszro</span> (<span class="id" type="var">scc</span> <span class="id" type="var">t<sub>1</sub></span>)) <span class="nowrap"><span style='font-size:85%;'><span style='vertical-align:6%;'><span style='letter-spacing:-.2em;'>-</span><span style='letter-spacing:-.2em;'>-</span></span>&gt;</span></span> <span class="id" type="var">fls</span><br/>
&nbsp;&nbsp;| <span class="id" type="var">ST_Iszro</span> : <span style='font-size:120%;'>&forall;</span><span class="id" type="var">t<sub>1</sub></span> <span class="id" type="var">t<sub>1</sub>'</span>,<br/>
&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;<span class="id" type="var">t<sub>1</sub></span> <span class="nowrap"><span style='font-size:85%;'><span style='vertical-align:6%;'><span style='letter-spacing:-.2em;'>-</span><span style='letter-spacing:-.2em;'>-</span></span>&gt;</span></span> <span class="id" type="var">t<sub>1</sub>'</span> →<br/>
&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;(<span class="id" type="var">iszro</span> <span class="id" type="var">t<sub>1</sub></span>) <span class="nowrap"><span style='font-size:85%;'><span style='vertical-align:6%;'><span style='letter-spacing:-.2em;'>-</span><span style='letter-spacing:-.2em;'>-</span></span>&gt;</span></span> (<span class="id" type="var">iszro</span> <span class="id" type="var">t<sub>1</sub>'</span>)<br/>
<br/>
<span class="id" type="keyword">where</span> "t<sub>1</sub> '<span class="nowrap"><span style='font-size:85%;'><span style='vertical-align:6%;'><span style='letter-spacing:-.2em;'>-</span><span style='letter-spacing:-.2em;'>-</span></span>&gt;</span></span>' t<sub>2</sub>" := (<span class="id" type="var">step</span> <span class="id" type="var">t<sub>1</sub></span> <span class="id" type="var">t<sub>2</sub></span>).<br/><hr class='doublespaceincode'/>
<span class="id" type="keyword">Hint</span> <span class="id" type="var">Constructors</span> <span class="id" type="var">step</span>.<br/>
</div>

<div class="doc">
请注意 <span class="inlinecode"><span class="id" type="var">step</span></span> 关系并不在意步进表达式是否有全局意义——它只是检查<b>下一步</b>
    的归约操作是否在正确的操作对象上。比如，项 <span class="inlinecode"><span class="id" type="var">succ</span></span> <span class="inlinecode"><span class="id" type="var">true</span></span>
    无法前进一步，但这个几乎显然无意义的项

<div class="paragraph"> </div>

<div class="code code-tight">
&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;<span class="id" type="var">scc</span>&nbsp;(<span class="id" type="var">test</span>&nbsp;<span class="id" type="var">tru</span>&nbsp;<span class="id" type="keyword">then</span>&nbsp;<span class="id" type="var">tru</span>&nbsp;<span class="id" type="keyword">else</span>&nbsp;<span class="id" type="var">tru</span>)
<div class="paragraph"> </div>

</div>
    却可以前进一步（注意是在卡住之前）。 
</div>

<div class="doc">
<a name="lab177"></a><h2 class="section">正规式和值</h2>

<div class="paragraph"> </div>

 首先值得注意的是 <a href="Smallstep.html"><span class="inlineref">Smallstep</span></a> 一章中的强可进性定理对这里的 <span class="inlinecode"><span class="id" type="var">step</span></span>
    归约并不成立。也即，有一些项是正规式（他们无法再前进一步），但却不是值（因为
    我们还没有把他们包括进潜在“归约结果”的定义中）。这样的项<b>卡住了</b>。 
</div>
<div class="code code-tight">

<span class="id" type="keyword">Notation</span> <span class="id" type="var">step_normal_form</span> := (<span class="id" type="var">normal_form</span> <span class="id" type="var">step</span>).<br/><hr class='doublespaceincode'/>
<span class="id" type="keyword">Definition</span> <span class="id" type="var">stuck</span> (<span class="id" type="var">t</span> : <span class="id" type="var">tm</span>) : <span class="id" type="keyword">Prop</span> :=<br/>
&nbsp;&nbsp;<span class="id" type="var">step_normal_form</span> <span class="id" type="var">t</span> ∧ ¬<span class="id" type="var">value</span> <span class="id" type="var">t</span>.<br/><hr class='doublespaceincode'/>
<span class="id" type="keyword">Hint</span> <span class="id" type="keyword">Unfold</span> <span class="id" type="var">stuck</span>.<br/>
</div>

<div class="doc">
<a name="lab178"></a><h4 class="section">练习：2 星, standard (some_term_is_stuck)</h4>

</div>
<div class="code code-space">
<span class="id" type="keyword">Example</span> <span class="id" type="var">some_term_is_stuck</span> :<br/>
&nbsp;&nbsp;<span style='font-size:120%;'>&exist;</span><span class="id" type="var">t</span>, <span class="id" type="var">stuck</span> <span class="id" type="var">t</span>.<br/>
<span class="id" type="keyword">Proof</span>.<br/>
&nbsp;&nbsp;<span class="comment">(*&nbsp;请在此处解答&nbsp;*)</span> <span class="id" type="var">Admitted</span>.<br/>
</div>

<span class="proofbox">&#9744;</span> 
<div class="doc less-space">
<div class="paragraph"> </div>

 然而，值和正规式在这个语言中<b>并不</b>相同，值的集合被包括在正规式的集合中。
    这一点很重要，因为这说明我们没有不小心定义了一些仍然能前进一步的值。
<div class="paragraph"> </div>

<a name="lab179"></a><h4 class="section">练习：3 星, standard (value_is_nf)</h4>

</div>
<div class="code code-space">
<span class="id" type="keyword">Lemma</span> <span class="id" type="var">value_is_nf</span> : <span style='font-size:120%;'>&forall;</span><span class="id" type="var">t</span>,<br/>
&nbsp;&nbsp;<span class="id" type="var">value</span> <span class="id" type="var">t</span> → <span class="id" type="var">step_normal_form</span> <span class="id" type="var">t</span>.<br/>
<div class="togglescript" id="proofcontrol1" onclick="toggleDisplay('proof1');toggleDisplay('proofcontrol1')"><span class="show"></span></div>
<div class="proofscript" id="proof1" onclick="toggleDisplay('proof1');toggleDisplay('proofcontrol1')">
<span class="id" type="keyword">Proof</span>.<br/>
&nbsp;&nbsp;<span class="comment">(*&nbsp;请在此处解答&nbsp;*)</span> <span class="id" type="var">Admitted</span>.<br/>
</div>
</div>

<div class="doc">
（提示：在证明中的某个地方，你需要使用归纳来推理某个项，这个项已知是数值。
    归纳可以对项本身进行，也可以对它是数值这个证据进行。两种方法均可完成证明，
    但你发现一种要比另一种稍微简短一点。作为练习，请尝试使用这两种方法完成证明。） <span class="proofbox">&#9744;</span> 
<div class="paragraph"> </div>

<a name="lab180"></a><h4 class="section">练习：3 星, standard, optional (step_deterministic)</h4>
 使用 <span class="inlinecode"><span class="id" type="var">value_is_nf</span></span> 来证明 <span class="inlinecode"><span class="id" type="var">step</span></span> 关系是确定的。
</div>
<div class="code code-tight">

<span class="id" type="keyword">Theorem</span> <span class="id" type="var">step_deterministic</span>:<br/>
&nbsp;&nbsp;<span class="id" type="var">deterministic</span> <span class="id" type="var">step</span>.<br/>
<span class="id" type="keyword">Proof</span> <span class="id" type="keyword">with</span> <span class="id" type="tactic">eauto</span>.<br/>
&nbsp;&nbsp;<span class="comment">(*&nbsp;请在此处解答&nbsp;*)</span> <span class="id" type="var">Admitted</span>.<br/>
</div>

<span class="proofbox">&#9744;</span> 

<div class="doc">
<a name="lab181"></a><h2 class="section">定型</h2>

<div class="paragraph"> </div>

 下一个重要的观察是，尽管这个语言中有卡住的项，他们总是以混合了
    布尔值和数字的方式变得完全没有意义，我们也<b>不想</b>为他们赋予意义。
    通过定义<b>类型关系（typing relation）</b>关联起项和他们最终结果的
    类型（数字或布尔值），我们可以容易地排除这些劣型（ill-typed）项。
</div>
<div class="code code-tight">

<span class="id" type="keyword">Inductive</span> <span class="id" type="var">ty</span> : <span class="id" type="keyword">Type</span> :=<br/>
&nbsp;&nbsp;| <span class="id" type="var">Bool</span> : <span class="id" type="var">ty</span><br/>
&nbsp;&nbsp;| <span class="id" type="var">Nat</span> : <span class="id" type="var">ty</span>.<br/>
</div>

<div class="doc">
在非形式化的记号中，类型关系经常写做 <span class="inlinecode">&#x22A2;</span> <span class="inlinecode"><span class="id" type="var">t</span></span> <span class="inlinecode">&#x2208;</span> <span class="inlinecode"><span class="id" type="var">T</span></span>，并读做“<span class="inlinecode"><span class="id" type="var">t</span></span> 有类型 <span class="inlinecode"><span class="id" type="var">T</span></span>”。
    <span class="inlinecode">&#x22A2;</span> 符号叫做“十字转门（turnstile）”。下面，我们会看到更加丰富的类型关系，其中
    我们会在 <span class="inlinecode">&#x22A2;</span> 左侧添加一个或多个“上下文（context）”。目前暂时来说，上下文总是空的。  <center><table class="infrule">
<tr class="infruleassumption">
  <td class="infrule">&nbsp;&nbsp;</td>
  <td class="infrulenamecol" rowspan="3">
    (T_Tru) &nbsp;
  </td></tr>
<tr class="infrulemiddle">
  <td class="infrule"><hr /></td>
</tr>
<tr class="infruleassumption">
  <td class="infrule">&#x22A2;&nbsp;tru&nbsp;&#x2208;&nbsp;Bool</td>
  <td></td>
</td>
</table></center><center><table class="infrule">
<tr class="infruleassumption">
  <td class="infrule">&nbsp;&nbsp;</td>
  <td class="infrulenamecol" rowspan="3">
    (T_Fls) &nbsp;
  </td></tr>
<tr class="infrulemiddle">
  <td class="infrule"><hr /></td>
</tr>
<tr class="infruleassumption">
  <td class="infrule">&#x22A2;&nbsp;fls&nbsp;&#x2208;&nbsp;Bool</td>
  <td></td>
</td>
</table></center><center><table class="infrule">
<tr class="infruleassumption">
  <td class="infrule">&#x22A2;&nbsp;t<sub>1</sub>&nbsp;&#x2208;&nbsp;Bool&nbsp;&nbsp;&nbsp;&nbsp;&#x22A2;&nbsp;t<sub>2</sub>&nbsp;&#x2208;&nbsp;T&nbsp;&nbsp;&nbsp;&nbsp;&#x22A2;&nbsp;t<sub>3</sub>&nbsp;&#x2208;&nbsp;T</td>
  <td class="infrulenamecol" rowspan="3">
    (T_Test) &nbsp;
  </td></tr>
<tr class="infrulemiddle">
  <td class="infrule"><hr /></td>
</tr>
<tr class="infruleassumption">
  <td class="infrule">&#x22A2;&nbsp;test&nbsp;t<sub>1</sub>&nbsp;then&nbsp;t<sub>2</sub>&nbsp;else&nbsp;t<sub>3</sub>&nbsp;&#x2208;&nbsp;T</td>
  <td></td>
</td>
</table></center><center><table class="infrule">
<tr class="infruleassumption">
  <td class="infrule">&nbsp;&nbsp;</td>
  <td class="infrulenamecol" rowspan="3">
    (T_Zro) &nbsp;
  </td></tr>
<tr class="infrulemiddle">
  <td class="infrule"><hr /></td>
</tr>
<tr class="infruleassumption">
  <td class="infrule">&#x22A2;&nbsp;zro&nbsp;&#x2208;&nbsp;Nat</td>
  <td></td>
</td>
</table></center><center><table class="infrule">
<tr class="infruleassumption">
  <td class="infrule">&#x22A2;&nbsp;t<sub>1</sub>&nbsp;&#x2208;&nbsp;Nat</td>
  <td class="infrulenamecol" rowspan="3">
    (T_Scc) &nbsp;
  </td></tr>
<tr class="infrulemiddle">
  <td class="infrule"><hr /></td>
</tr>
<tr class="infruleassumption">
  <td class="infrule">&#x22A2;&nbsp;scc&nbsp;t<sub>1</sub>&nbsp;&#x2208;&nbsp;Nat</td>
  <td></td>
</td>
</table></center><center><table class="infrule">
<tr class="infruleassumption">
  <td class="infrule">&#x22A2;&nbsp;t<sub>1</sub>&nbsp;&#x2208;&nbsp;Nat</td>
  <td class="infrulenamecol" rowspan="3">
    (T_Prd) &nbsp;
  </td></tr>
<tr class="infrulemiddle">
  <td class="infrule"><hr /></td>
</tr>
<tr class="infruleassumption">
  <td class="infrule">&#x22A2;&nbsp;prd&nbsp;t<sub>1</sub>&nbsp;&#x2208;&nbsp;Nat</td>
  <td></td>
</td>
</table></center><center><table class="infrule">
<tr class="infruleassumption">
  <td class="infrule">&#x22A2;&nbsp;t<sub>1</sub>&nbsp;&#x2208;&nbsp;Nat</td>
  <td class="infrulenamecol" rowspan="3">
    (T_IsZro) &nbsp;
  </td></tr>
<tr class="infrulemiddle">
  <td class="infrule"><hr /></td>
</tr>
<tr class="infruleassumption">
  <td class="infrule">&#x22A2;&nbsp;iszro&nbsp;t<sub>1</sub>&nbsp;&#x2208;&nbsp;Bool</td>
  <td></td>
</td>
</table></center>
</div>
<div class="code code-tight">

<span class="id" type="keyword">Reserved Notation</span> "'&#x22A2;' t '&#x2208;' T" (<span class="id" type="tactic">at</span> <span class="id" type="var">level</span> 40).<br/><hr class='doublespaceincode'/>
<span class="id" type="keyword">Inductive</span> <span class="id" type="var">has_type</span> : <span class="id" type="var">tm</span> → <span class="id" type="var">ty</span> → <span class="id" type="keyword">Prop</span> :=<br/>
&nbsp;&nbsp;| <span class="id" type="var">T_Tru</span> :<br/>
&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&#x22A2; <span class="id" type="var">tru</span> &#x2208; <span class="id" type="var">Bool</span><br/>
&nbsp;&nbsp;| <span class="id" type="var">T_Fls</span> :<br/>
&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&#x22A2; <span class="id" type="var">fls</span> &#x2208; <span class="id" type="var">Bool</span><br/>
&nbsp;&nbsp;| <span class="id" type="var">T_Test</span> : <span style='font-size:120%;'>&forall;</span><span class="id" type="var">t<sub>1</sub></span> <span class="id" type="var">t<sub>2</sub></span> <span class="id" type="var">t<sub>3</sub></span> <span class="id" type="var">T</span>,<br/>
&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&#x22A2; <span class="id" type="var">t<sub>1</sub></span> &#x2208; <span class="id" type="var">Bool</span> →<br/>
&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&#x22A2; <span class="id" type="var">t<sub>2</sub></span> &#x2208; <span class="id" type="var">T</span> →<br/>
&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&#x22A2; <span class="id" type="var">t<sub>3</sub></span> &#x2208; <span class="id" type="var">T</span> →<br/>
&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&#x22A2; <span class="id" type="var">test</span> <span class="id" type="var">t<sub>1</sub></span> <span class="id" type="var">t<sub>2</sub></span> <span class="id" type="var">t<sub>3</sub></span> &#x2208; <span class="id" type="var">T</span><br/>
&nbsp;&nbsp;| <span class="id" type="var">T_Zro</span> :<br/>
&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&#x22A2; <span class="id" type="var">zro</span> &#x2208; <span class="id" type="var">Nat</span><br/>
&nbsp;&nbsp;| <span class="id" type="var">T_Scc</span> : <span style='font-size:120%;'>&forall;</span><span class="id" type="var">t<sub>1</sub></span>,<br/>
&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&#x22A2; <span class="id" type="var">t<sub>1</sub></span> &#x2208; <span class="id" type="var">Nat</span> →<br/>
&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&#x22A2; <span class="id" type="var">scc</span> <span class="id" type="var">t<sub>1</sub></span> &#x2208; <span class="id" type="var">Nat</span><br/>
&nbsp;&nbsp;| <span class="id" type="var">T_Prd</span> : <span style='font-size:120%;'>&forall;</span><span class="id" type="var">t<sub>1</sub></span>,<br/>
&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&#x22A2; <span class="id" type="var">t<sub>1</sub></span> &#x2208; <span class="id" type="var">Nat</span> →<br/>
&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&#x22A2; <span class="id" type="var">prd</span> <span class="id" type="var">t<sub>1</sub></span> &#x2208; <span class="id" type="var">Nat</span><br/>
&nbsp;&nbsp;| <span class="id" type="var">T_Iszro</span> : <span style='font-size:120%;'>&forall;</span><span class="id" type="var">t<sub>1</sub></span>,<br/>
&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&#x22A2; <span class="id" type="var">t<sub>1</sub></span> &#x2208; <span class="id" type="var">Nat</span> →<br/>
&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&#x22A2; <span class="id" type="var">iszro</span> <span class="id" type="var">t<sub>1</sub></span> &#x2208; <span class="id" type="var">Bool</span><br/>
<br/>
<span class="id" type="keyword">where</span> "'&#x22A2;' t '&#x2208;' T" := (<span class="id" type="var">has_type</span> <span class="id" type="var">t</span> <span class="id" type="var">T</span>).<br/><hr class='doublespaceincode'/>
<span class="id" type="keyword">Hint</span> <span class="id" type="var">Constructors</span> <span class="id" type="var">has_type</span>.<br/><hr class='doublespaceincode'/>
<span class="id" type="keyword">Example</span> <span class="id" type="var">has_type_1</span> :<br/>
&nbsp;&nbsp;&#x22A2; <span class="id" type="var">test</span> <span class="id" type="var">fls</span> <span class="id" type="var">zro</span> (<span class="id" type="var">scc</span> <span class="id" type="var">zro</span>) &#x2208; <span class="id" type="var">Nat</span>.<br/>
<span class="id" type="keyword">Proof</span>.<br/>
&nbsp;&nbsp;<span class="id" type="tactic">apply</span> <span class="id" type="var">T_Test</span>.<br/>
&nbsp;&nbsp;&nbsp;&nbsp;- <span class="id" type="tactic">apply</span> <span class="id" type="var">T_Fls</span>.<br/>
&nbsp;&nbsp;&nbsp;&nbsp;- <span class="id" type="tactic">apply</span> <span class="id" type="var">T_Zro</span>.<br/>
&nbsp;&nbsp;&nbsp;&nbsp;- <span class="id" type="tactic">apply</span> <span class="id" type="var">T_Scc</span>.<br/>
&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;+ <span class="id" type="tactic">apply</span> <span class="id" type="var">T_Zro</span>.<br/>
<span class="id" type="keyword">Qed</span>.<br/>
</div>

<div class="doc">
（因为我们在提示数据库（hint database）中包括了类型关系的所有构造子，
    因此 <span class="inlinecode"><span class="id" type="tactic">auto</span></span> 策略可以自动完成这个证明。）
<div class="paragraph"> </div>

 重要的一点是认识到类型关系是一个<b>保守的（conservative）</b>
    （或<b>静态的（static）</b>）近似：它不考虑项被归约时会发生什么——特别地，
    它并不计算项的正规式的类型。 
</div>
<div class="code code-tight">

<span class="id" type="keyword">Example</span> <span class="id" type="var">has_type_not</span> :<br/>
&nbsp;&nbsp;¬( &#x22A2; <span class="id" type="var">test</span> <span class="id" type="var">fls</span> <span class="id" type="var">zro</span> <span class="id" type="var">tru</span> &#x2208; <span class="id" type="var">Bool</span> ).<br/>
<div class="togglescript" id="proofcontrol2" onclick="toggleDisplay('proof2');toggleDisplay('proofcontrol2')"><span class="show"></span></div>
<div class="proofscript" id="proof2" onclick="toggleDisplay('proof2');toggleDisplay('proofcontrol2')">
<span class="id" type="keyword">Proof</span>.<br/>
&nbsp;&nbsp;<span class="id" type="tactic">intros</span> <span class="id" type="var">Contra</span>. <span class="id" type="var">solve_by_inverts</span> 2. <span class="id" type="keyword">Qed</span>.<br/>
</div>
</div>

<div class="doc">
<a name="lab182"></a><h4 class="section">练习：1 星, standard, optional (scc_hastype_nat__hastype_nat)</h4>

</div>
<div class="code code-space">
<span class="id" type="keyword">Example</span> <span class="id" type="var">scc_hastype_nat__hastype_nat</span> : <span style='font-size:120%;'>&forall;</span><span class="id" type="var">t</span>,<br/>
&nbsp;&nbsp;&#x22A2; <span class="id" type="var">scc</span> <span class="id" type="var">t</span> &#x2208; <span class="id" type="var">Nat</span> →<br/>
&nbsp;&nbsp;&#x22A2; <span class="id" type="var">t</span> &#x2208; <span class="id" type="var">Nat</span>.<br/>
<span class="id" type="keyword">Proof</span>.<br/>
&nbsp;&nbsp;<span class="comment">(*&nbsp;请在此处解答&nbsp;*)</span> <span class="id" type="var">Admitted</span>.<br/>
</div>

<span class="proofbox">&#9744;</span> 

<div class="doc">
<a name="lab183"></a><h3 class="section">典范形式</h3>

<div class="paragraph"> </div>

 下面的两个引理作为基础性质表达了布尔值和数值的定义同类型关系相一致。
</div>
<div class="code code-tight">

<span class="id" type="keyword">Lemma</span> <span class="id" type="var">bool_canonical</span> : <span style='font-size:120%;'>&forall;</span><span class="id" type="var">t</span>,<br/>
&nbsp;&nbsp;&#x22A2; <span class="id" type="var">t</span> &#x2208; <span class="id" type="var">Bool</span> → <span class="id" type="var">value</span> <span class="id" type="var">t</span> → <span class="id" type="var">bvalue</span> <span class="id" type="var">t</span>.<br/>
<div class="togglescript" id="proofcontrol3" onclick="toggleDisplay('proof3');toggleDisplay('proofcontrol3')"><span class="show"></span></div>
<div class="proofscript" id="proof3" onclick="toggleDisplay('proof3');toggleDisplay('proofcontrol3')">
<span class="id" type="keyword">Proof</span>.<br/>
&nbsp;&nbsp;<span class="id" type="tactic">intros</span> <span class="id" type="var">t</span> <span class="id" type="var">HT</span> [<span class="id" type="var">Hb</span> | <span class="id" type="var">Hn</span>].<br/>
&nbsp;&nbsp;- <span class="id" type="tactic">assumption</span>.<br/>
&nbsp;&nbsp;- <span class="id" type="tactic">induction</span> <span class="id" type="var">Hn</span>; <span class="id" type="tactic">inversion</span> <span class="id" type="var">HT</span>; <span class="id" type="tactic">auto</span>.<br/>
<span class="id" type="keyword">Qed</span>.<br/>
</div>

<br/>
<span class="id" type="keyword">Lemma</span> <span class="id" type="var">nat_canonical</span> : <span style='font-size:120%;'>&forall;</span><span class="id" type="var">t</span>,<br/>
&nbsp;&nbsp;&#x22A2; <span class="id" type="var">t</span> &#x2208; <span class="id" type="var">Nat</span> → <span class="id" type="var">value</span> <span class="id" type="var">t</span> → <span class="id" type="var">nvalue</span> <span class="id" type="var">t</span>.<br/>
<div class="togglescript" id="proofcontrol4" onclick="toggleDisplay('proof4');toggleDisplay('proofcontrol4')"><span class="show"></span></div>
<div class="proofscript" id="proof4" onclick="toggleDisplay('proof4');toggleDisplay('proofcontrol4')">
<span class="id" type="keyword">Proof</span>.<br/>
&nbsp;&nbsp;<span class="id" type="tactic">intros</span> <span class="id" type="var">t</span> <span class="id" type="var">HT</span> [<span class="id" type="var">Hb</span> | <span class="id" type="var">Hn</span>].<br/>
&nbsp;&nbsp;- <span class="id" type="tactic">inversion</span> <span class="id" type="var">Hb</span>; <span class="id" type="tactic">subst</span>; <span class="id" type="tactic">inversion</span> <span class="id" type="var">HT</span>.<br/>
&nbsp;&nbsp;- <span class="id" type="tactic">assumption</span>.<br/>
<span class="id" type="keyword">Qed</span>.<br/>
</div>
</div>

<div class="doc">
<a name="lab184"></a><h2 class="section">可进性</h2>

<div class="paragraph"> </div>

 类型关系具有两个十分重要的性质。第一个是良型（well-typed）的正规式不会卡住——或者，反过来说，
    如果一个项是良型的，那么它要么是一个值，要么可以至少前进一步。我们把这个性质叫做
    <b>可进性（progress）</b>。 
<div class="paragraph"> </div>

<a name="lab185"></a><h4 class="section">练习：3 星, standard (finish_progress)</h4>

</div>
<div class="code code-space">
<span class="id" type="keyword">Theorem</span> <span class="id" type="tactic">progress</span> : <span style='font-size:120%;'>&forall;</span><span class="id" type="var">t</span> <span class="id" type="var">T</span>,<br/>
&nbsp;&nbsp;&#x22A2; <span class="id" type="var">t</span> &#x2208; <span class="id" type="var">T</span> →<br/>
&nbsp;&nbsp;<span class="id" type="var">value</span> <span class="id" type="var">t</span> ∨ <span style='font-size:120%;'>&exist;</span><span class="id" type="var">t'</span>, <span class="id" type="var">t</span> <span class="nowrap"><span style='font-size:85%;'><span style='vertical-align:6%;'><span style='letter-spacing:-.2em;'>-</span><span style='letter-spacing:-.2em;'>-</span></span>&gt;</span></span> <span class="id" type="var">t'</span>.<br/>
</div>

<div class="doc">
请完成 <span class="inlinecode"><span class="id" type="tactic">progress</span></span> 性质的形式化证明。（在开始前请确保你理解了下一个练习中的非
    形式化证明——这会节省很多你的时间。）
</div>
<div class="code code-tight">
<div class="togglescript" id="proofcontrol5" onclick="toggleDisplay('proof5');toggleDisplay('proofcontrol5')"><span class="show"></span></div>
<div class="proofscript" id="proof5" onclick="toggleDisplay('proof5');toggleDisplay('proofcontrol5')">
<span class="id" type="keyword">Proof</span> <span class="id" type="keyword">with</span> <span class="id" type="tactic">auto</span>.<br/>
&nbsp;&nbsp;<span class="id" type="tactic">intros</span> <span class="id" type="var">t</span> <span class="id" type="var">T</span> <span class="id" type="var">HT</span>.<br/>
&nbsp;&nbsp;<span class="id" type="tactic">induction</span> <span class="id" type="var">HT</span>...<br/>
&nbsp;&nbsp;<span class="comment">(*&nbsp;对于显然是值的情形，比如&nbsp;T_Tru&nbsp;和&nbsp;T_Fls，我们直接使用&nbsp;auto&nbsp;完成。*)</span><br/>
&nbsp;&nbsp;- <span class="comment">(*&nbsp;T_Test&nbsp;*)</span><br/>
&nbsp;&nbsp;&nbsp;&nbsp;<span class="id" type="var">right</span>. <span class="id" type="tactic">inversion</span> <span class="id" type="var">IHHT1</span>; <span class="id" type="tactic">clear</span> <span class="id" type="var">IHHT1</span>.<br/>
&nbsp;&nbsp;&nbsp;&nbsp;+ <span class="comment">(*&nbsp;t<sub>1</sub>&nbsp;是值&nbsp;*)</span><br/>
&nbsp;&nbsp;&nbsp;&nbsp;<span class="id" type="tactic">apply</span> (<span class="id" type="var">bool_canonical</span> <span class="id" type="var">t<sub>1</sub></span> <span class="id" type="var">HT<sub>1</sub></span>) <span class="id" type="keyword">in</span> <span class="id" type="var">H</span>.<br/>
&nbsp;&nbsp;&nbsp;&nbsp;<span class="id" type="tactic">inversion</span> <span class="id" type="var">H</span>; <span class="id" type="tactic">subst</span>; <span class="id" type="tactic">clear</span> <span class="id" type="var">H</span>.<br/>
&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;<span style='font-size:120%;'>&exist;</span><span class="id" type="var">t<sub>2</sub></span>...<br/>
&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;<span style='font-size:120%;'>&exist;</span><span class="id" type="var">t<sub>3</sub></span>...<br/>
&nbsp;&nbsp;&nbsp;&nbsp;+ <span class="comment">(*&nbsp;t<sub>1</sub>&nbsp;可前进一步&nbsp;*)</span><br/>
&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;<span class="id" type="tactic">inversion</span> <span class="id" type="var">H</span> <span class="id" type="keyword">as</span> [<span class="id" type="var">t<sub>1</sub>'</span> <span class="id" type="var">H<sub>1</sub></span>].<br/>
&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;<span style='font-size:120%;'>&exist;</span>(<span class="id" type="var">test</span> <span class="id" type="var">t<sub>1</sub>'</span> <span class="id" type="var">t<sub>2</sub></span> <span class="id" type="var">t<sub>3</sub></span>)...<br/>
&nbsp;&nbsp;<span class="comment">(*&nbsp;请在此处解答&nbsp;*)</span> <span class="id" type="var">Admitted</span>.<br/>
</div>
</div>

<span class="proofbox">&#9744;</span> 
<div class="doc less-space">
<div class="paragraph"> </div>

<a name="lab186"></a><h4 class="section">练习：3 星, advanced (finish_progress_informal)</h4>
 请完成非形式化的证明： 
<div class="paragraph"> </div>

 <b>定理</b>：如果 <span class="inlinecode">&#x22A2;</span> <span class="inlinecode"><span class="id" type="var">t</span></span> <span class="inlinecode">&#x2208;</span> <span class="inlinecode"><span class="id" type="var">T</span></span>，那么 <span class="inlinecode"><span class="id" type="var">t</span></span> 要么是值，要么存在某个 <span class="inlinecode"><span class="id" type="var">t'</span></span> 使 <span class="inlinecode"><span class="id" type="var">t</span></span> <span class="inlinecode"><span class="nowrap"><span style='font-size:85%;'><span style='vertical-align:6%;'><span style='letter-spacing:-.2em;'>-</span><span style='letter-spacing:-.2em;'>-</span></span>&gt;</span></span></span> <span class="inlinecode"><span class="id" type="var">t'</span></span>。
<div class="paragraph"> </div>

 <b>证明</b>：对 <span class="inlinecode">&#x22A2;</span> <span class="inlinecode"><span class="id" type="var">t</span></span> <span class="inlinecode">&#x2208;</span> <span class="inlinecode"><span class="id" type="var">T</span></span> 的导出式进行归纳。

<div class="paragraph"> </div>

<ul class="doclist">
<li> 如果导出式的最后一条规则是 <span class="inlinecode"><span class="id" type="var">T_Test</span></span>，那么 <span class="inlinecode"><span class="id" type="var">t</span></span> <span class="inlinecode">=</span> <span class="inlinecode"><span class="id" type="var">test</span></span> <span class="inlinecode"><span class="id" type="var">t<sub>1</sub></span></span> <span class="inlinecode"><span class="id" type="keyword">then</span></span> <span class="inlinecode"><span class="id" type="var">t<sub>2</sub></span></span> <span class="inlinecode"><span class="id" type="keyword">else</span></span> <span class="inlinecode"><span class="id" type="var">t<sub>3</sub></span></span>，
        其中 <span class="inlinecode">&#x22A2;</span> <span class="inlinecode"><span class="id" type="var">t<sub>1</sub></span></span> <span class="inlinecode">&#x2208;</span> <span class="inlinecode"><span class="id" type="var">Bool</span></span>，<span class="inlinecode">&#x22A2;</span> <span class="inlinecode"><span class="id" type="var">t<sub>2</sub></span></span> <span class="inlinecode">&#x2208;</span> <span class="inlinecode"><span class="id" type="var">T</span></span> 以及 <span class="inlinecode">&#x22A2;</span> <span class="inlinecode"><span class="id" type="var">t<sub>3</sub></span></span> <span class="inlinecode">&#x2208;</span> <span class="inlinecode"><span class="id" type="var">T</span></span>。
        根据归纳假设，<span class="inlinecode"><span class="id" type="var">t<sub>1</sub></span></span> 要么是值，要么可前进一步到某个 <span class="inlinecode"><span class="id" type="var">t<sub>1</sub>'</span></span>。

<div class="paragraph"> </div>


</li>
<li> 如果 <span class="inlinecode"><span class="id" type="var">t<sub>1</sub></span></span> 是值，那么根据典范形式（canonical forms）引理以及
        <span class="inlinecode">&#x22A2;</span> <span class="inlinecode"><span class="id" type="var">t<sub>1</sub></span></span> <span class="inlinecode">&#x2208;</span> <span class="inlinecode"><span class="id" type="var">Bool</span></span> 的事实，可得 <span class="inlinecode"><span class="id" type="var">t<sub>1</sub></span></span> 是一个 <span class="inlinecode"><span class="id" type="var">bvalue</span></span>——也即，
        它要么是 <span class="inlinecode"><span class="id" type="var">tru</span></span> 要么是 <span class="inlinecode"><span class="id" type="var">fls</span></span>。如果 <span class="inlinecode"><span class="id" type="var">t<sub>1</sub></span></span> <span class="inlinecode">=</span> <span class="inlinecode"><span class="id" type="var">tru</span></span>，由 <span class="inlinecode"><span class="id" type="var">ST_TestTru</span></span>
        可得 <span class="inlinecode"><span class="id" type="var">t</span></span> 前进到 <span class="inlinecode"><span class="id" type="var">t<sub>2</sub></span></span>；而当 <span class="inlinecode"><span class="id" type="var">t<sub>1</sub></span></span> <span class="inlinecode">=</span> <span class="inlinecode"><span class="id" type="var">fls</span></span> 时，由 <span class="inlinecode"><span class="id" type="var">ST_TestFls</span></span>
        可得 <span class="inlinecode"><span class="id" type="var">t</span></span> 前进到 <span class="inlinecode"><span class="id" type="var">t<sub>3</sub></span></span>。不论哪种情况，<span class="inlinecode"><span class="id" type="var">t</span></span> 都可以前进一步，这是我们
        想要证明的。

<div class="paragraph"> </div>


</li>
<li> 如果 <span class="inlinecode"><span class="id" type="var">t<sub>1</sub></span></span> 自己可以前进一步，那么根据 <span class="inlinecode"><span class="id" type="var">ST_Test</span></span> 可得 <span class="inlinecode"><span class="id" type="var">t</span></span> 也可以。

<div class="paragraph"> </div>


<div class="paragraph"> </div>


</li>
<li> <span class="comment">(*&nbsp;请在此处解答&nbsp;*)</span><br/>

</li>
</ul>
 
</div>
<div class="code code-tight">
<span class="comment">(*&nbsp;请勿修改下面这一行：&nbsp;*)</span><br/>
<span class="id" type="keyword">Definition</span> <span class="id" type="var">manual_grade_for_finish_progress_informal</span> : <span class="id" type="var">option</span> (<span class="id" type="var">nat</span>*<span class="id" type="var">string</span>) := <span class="id" type="var">None</span>.<br/>
</div>

<span class="proofbox">&#9744;</span> 
<div class="doc less-space">
<div class="paragraph"> </div>

 这个定理要比 <a href="Smallstep.html"><span class="inlineref">Smallstep</span></a> 一章中的强可进性定理更有趣一些，在强可进性定理
    中<b>全部</b>的正规式都是值。这里项可以卡住，但仅当它为劣型时。 
</div>

<div class="doc">
<a name="lab187"></a><h2 class="section">保型性</h2>

<div class="paragraph"> </div>

 关于类型的第二个重要性质是，当一个良型项可前进一步时，其结果也是一个良型项。
<div class="paragraph"> </div>

<a name="lab188"></a><h4 class="section">练习：2 星, standard (finish_preservation)</h4>

</div>
<div class="code code-space">
<span class="id" type="keyword">Theorem</span> <span class="id" type="var">preservation</span> : <span style='font-size:120%;'>&forall;</span><span class="id" type="var">t</span> <span class="id" type="var">t'</span> <span class="id" type="var">T</span>,<br/>
&nbsp;&nbsp;&#x22A2; <span class="id" type="var">t</span> &#x2208; <span class="id" type="var">T</span> →<br/>
&nbsp;&nbsp;<span class="id" type="var">t</span> <span class="nowrap"><span style='font-size:85%;'><span style='vertical-align:6%;'><span style='letter-spacing:-.2em;'>-</span><span style='letter-spacing:-.2em;'>-</span></span>&gt;</span></span> <span class="id" type="var">t'</span> →<br/>
&nbsp;&nbsp;&#x22A2; <span class="id" type="var">t'</span> &#x2208; <span class="id" type="var">T</span>.<br/>
</div>

<div class="doc">
请完成 <span class="inlinecode"><span class="id" type="var">preservation</span></span> 性质的形式化证明。（和上次一样，在开始前请确保你理解了
    下一个练习中的非形式化证明。） 
</div>
<div class="code code-tight">

<div class="togglescript" id="proofcontrol6" onclick="toggleDisplay('proof6');toggleDisplay('proofcontrol6')"><span class="show"></span></div>
<div class="proofscript" id="proof6" onclick="toggleDisplay('proof6');toggleDisplay('proofcontrol6')">
<span class="id" type="keyword">Proof</span> <span class="id" type="keyword">with</span> <span class="id" type="tactic">auto</span>.<br/>
&nbsp;&nbsp;<span class="id" type="tactic">intros</span> <span class="id" type="var">t</span> <span class="id" type="var">t'</span> <span class="id" type="var">T</span> <span class="id" type="var">HT</span> <span class="id" type="var">HE</span>.<br/>
&nbsp;&nbsp;<span class="id" type="tactic">generalize</span> <span class="id" type="tactic">dependent</span> <span class="id" type="var">t'</span>.<br/>
&nbsp;&nbsp;<span class="id" type="tactic">induction</span> <span class="id" type="var">HT</span>;<br/>
&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;<span class="comment">(*&nbsp;每个情形都需要引入一些东西&nbsp;*)</span><br/>
&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;<span class="id" type="tactic">intros</span> <span class="id" type="var">t'</span> <span class="id" type="var">HE</span>;<br/>
&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;<span class="comment">(*&nbsp;我们还需要处理一些不可能发生的情形&nbsp;*)</span><br/>
&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;<span class="id" type="tactic">try</span> <span class="id" type="var">solve_by_invert</span>.<br/>
&nbsp;&nbsp;&nbsp;&nbsp;- <span class="comment">(*&nbsp;T_Test&nbsp;*)</span> <span class="id" type="tactic">inversion</span> <span class="id" type="var">HE</span>; <span class="id" type="tactic">subst</span>; <span class="id" type="tactic">clear</span> <span class="id" type="var">HE</span>.<br/>
&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;+ <span class="comment">(*&nbsp;ST_TESTTru&nbsp;*)</span> <span class="id" type="tactic">assumption</span>.<br/>
&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;+ <span class="comment">(*&nbsp;ST_TestFls&nbsp;*)</span> <span class="id" type="tactic">assumption</span>.<br/>
&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;+ <span class="comment">(*&nbsp;ST_Test&nbsp;*)</span> <span class="id" type="tactic">apply</span> <span class="id" type="var">T_Test</span>; <span class="id" type="tactic">try</span> <span class="id" type="tactic">assumption</span>.<br/>
&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;<span class="id" type="tactic">apply</span> <span class="id" type="var">IHHT1</span>; <span class="id" type="tactic">assumption</span>.<br/>
&nbsp;&nbsp;&nbsp;&nbsp;<span class="comment">(*&nbsp;请在此处解答&nbsp;*)</span> <span class="id" type="var">Admitted</span>.<br/>
</div>
</div>

<span class="proofbox">&#9744;</span> 
<div class="doc less-space">
<div class="paragraph"> </div>

<a name="lab189"></a><h4 class="section">练习：3 星, advanced (finish_preservation_informal)</h4>
 请完成非形式化的证明： 
<div class="paragraph"> </div>

 <b>定理</b>：如果 <span class="inlinecode">&#x22A2;</span> <span class="inlinecode"><span class="id" type="var">t</span></span> <span class="inlinecode">&#x2208;</span> <span class="inlinecode"><span class="id" type="var">T</span></span> 且 <span class="inlinecode"><span class="id" type="var">t</span></span> <span class="inlinecode"><span class="nowrap"><span style='font-size:85%;'><span style='vertical-align:6%;'><span style='letter-spacing:-.2em;'>-</span><span style='letter-spacing:-.2em;'>-</span></span>&gt;</span></span></span> <span class="inlinecode"><span class="id" type="var">t'</span></span>，那么 <span class="inlinecode">&#x22A2;</span> <span class="inlinecode"><span class="id" type="var">t'</span></span> <span class="inlinecode">&#x2208;</span> <span class="inlinecode"><span class="id" type="var">T</span></span>。 
<div class="paragraph"> </div>

 <b>证明</b>：对 <span class="inlinecode">&#x22A2;</span> <span class="inlinecode"><span class="id" type="var">t</span></span> <span class="inlinecode">&#x2208;</span> <span class="inlinecode"><span class="id" type="var">T</span></span> 的导出式进行归纳。

<div class="paragraph"> </div>

<ul class="doclist">
<li> 如果导出式的最后一条规则是 <span class="inlinecode"><span class="id" type="var">T_Test</span></span>，那么 <span class="inlinecode"><span class="id" type="var">t</span></span> <span class="inlinecode">=</span> <span class="inlinecode"><span class="id" type="var">test</span></span> <span class="inlinecode"><span class="id" type="var">t<sub>1</sub></span></span>
        <span class="inlinecode"><span class="id" type="keyword">then</span></span> <span class="inlinecode"><span class="id" type="var">t<sub>2</sub></span></span> <span class="inlinecode"><span class="id" type="keyword">else</span></span> <span class="inlinecode"><span class="id" type="var">t<sub>3</sub></span></span>，其中 <span class="inlinecode">&#x22A2;</span> <span class="inlinecode"><span class="id" type="var">t<sub>1</sub></span></span> <span class="inlinecode">&#x2208;</span> <span class="inlinecode"><span class="id" type="var">Bool</span></span>， <span class="inlinecode">&#x22A2;</span> <span class="inlinecode"><span class="id" type="var">t<sub>2</sub></span></span> <span class="inlinecode">&#x2208;</span> <span class="inlinecode"><span class="id" type="var">T</span></span> 以及 <span class="inlinecode">&#x22A2;</span> <span class="inlinecode"><span class="id" type="var">t<sub>3</sub></span></span>
        <span class="inlinecode">&#x2208;</span> <span class="inlinecode"><span class="id" type="var">T</span></span>。

<div class="paragraph"> </div>

        请记着 <span class="inlinecode"><span class="id" type="var">t</span></span> 形如 <span class="inlinecode"><span class="id" type="var">test</span></span> <span class="inlinecode">...</span>，通过检查小步归约关系的规则，我们看到可以用来证明
        <span class="inlinecode"><span class="id" type="var">t</span></span> <span class="inlinecode"><span class="nowrap"><span style='font-size:85%;'><span style='vertical-align:6%;'><span style='letter-spacing:-.2em;'>-</span><span style='letter-spacing:-.2em;'>-</span></span>&gt;</span></span></span> <span class="inlinecode"><span class="id" type="var">t'</span></span> 的规则仅有 <span class="inlinecode"><span class="id" type="var">ST_TestTru</span></span>，<span class="inlinecode"><span class="id" type="var">ST_TestFls</span></span> 或者 <span class="inlinecode"><span class="id" type="var">ST_Test</span></span>。

<div class="paragraph"> </div>


</li>
<li> 如果最后的规则是 <span class="inlinecode"><span class="id" type="var">ST_TestTru</span></span>，那么 <span class="inlinecode"><span class="id" type="var">t'</span></span> <span class="inlinecode">=</span> <span class="inlinecode"><span class="id" type="var">t<sub>2</sub></span></span>。但是我们有
        <span class="inlinecode">&#x22A2;</span> <span class="inlinecode"><span class="id" type="var">t<sub>2</sub></span></span> <span class="inlinecode">&#x2208;</span> <span class="inlinecode"><span class="id" type="var">T</span></span>，所以证明完成。

<div class="paragraph"> </div>


</li>
<li> 如果最后的规则是 <span class="inlinecode"><span class="id" type="var">ST_TestFls</span></span>，那么 <span class="inlinecode"><span class="id" type="var">t'</span></span> <span class="inlinecode">=</span> <span class="inlinecode"><span class="id" type="var">t<sub>3</sub></span></span>。但是我们有
        <span class="inlinecode">&#x22A2;</span> <span class="inlinecode"><span class="id" type="var">t<sub>3</sub></span></span> <span class="inlinecode">&#x2208;</span> <span class="inlinecode"><span class="id" type="var">T</span></span>，所以证明完成。

<div class="paragraph"> </div>


</li>
<li> 如果最后的规则是 <span class="inlinecode"><span class="id" type="var">ST_Test</span></span>，那么 <span class="inlinecode"><span class="id" type="var">t'</span></span> <span class="inlinecode">=</span> <span class="inlinecode"><span class="id" type="var">test</span></span> <span class="inlinecode"><span class="id" type="var">t<sub>1</sub>'</span></span> <span class="inlinecode"><span class="id" type="keyword">then</span></span> <span class="inlinecode"><span class="id" type="var">t<sub>2</sub></span></span>
        <span class="inlinecode"><span class="id" type="keyword">else</span></span> <span class="inlinecode"><span class="id" type="var">t<sub>3</sub></span></span>，其中 <span class="inlinecode"><span class="id" type="var">t<sub>1</sub></span></span> <span class="inlinecode"><span class="nowrap"><span style='font-size:85%;'><span style='vertical-align:6%;'><span style='letter-spacing:-.2em;'>-</span><span style='letter-spacing:-.2em;'>-</span></span>&gt;</span></span></span> <span class="inlinecode"><span class="id" type="var">t<sub>1</sub>'</span></span>。我们知道 <span class="inlinecode">&#x22A2;</span> <span class="inlinecode"><span class="id" type="var">t<sub>1</sub></span></span> <span class="inlinecode">&#x2208;</span> <span class="inlinecode"><span class="id" type="var">Bool</span></span>，
        因此根据归纳假设可得 <span class="inlinecode">&#x22A2;</span> <span class="inlinecode"><span class="id" type="var">t<sub>1</sub>'</span></span> <span class="inlinecode">&#x2208;</span> <span class="inlinecode"><span class="id" type="var">Bool</span></span>。正如需要的那样，规则
        <span class="inlinecode"><span class="id" type="var">T_Test</span></span> 为我们提供了 <span class="inlinecode">&#x22A2;</span> <span class="inlinecode"><span class="id" type="var">test</span></span> <span class="inlinecode"><span class="id" type="var">t<sub>1</sub>'</span></span> <span class="inlinecode"><span class="id" type="keyword">then</span></span> <span class="inlinecode"><span class="id" type="var">t<sub>2</sub></span></span> <span class="inlinecode"><span class="id" type="keyword">else</span></span> <span class="inlinecode"><span class="id" type="var">t<sub>3</sub></span></span> <span class="inlinecode">&#x2208;</span> <span class="inlinecode"><span class="id" type="var">T</span></span>。

<div class="paragraph"> </div>


<div class="paragraph"> </div>


</li>
<li> <span class="comment">(*&nbsp;请在此处解答&nbsp;*)</span><br/>

</li>
</ul>

</div>
<div class="code code-tight">
<span class="comment">(*&nbsp;请勿修改下面这一行：&nbsp;*)</span><br/>
<span class="id" type="keyword">Definition</span> <span class="id" type="var">manual_grade_for_finish_preservation_informal</span> : <span class="id" type="var">option</span> (<span class="id" type="var">nat</span>*<span class="id" type="var">string</span>) := <span class="id" type="var">None</span>.<br/>
</div>

<span class="proofbox">&#9744;</span> 
<div class="doc less-space">
<div class="paragraph"> </div>

<a name="lab190"></a><h4 class="section">练习：3 星, standard (preservation_alternate_proof)</h4>
 现在请对<b>求值</b>导出式（而非类型导出式）进行归纳来证明保型性定理。
    请仔细阅读和思考上面证明中最开始的几行，确保你理解了他们是在做什么。
    本证明的开始部分类似，但并不完全一样。
</div>
<div class="code code-tight">

<span class="id" type="keyword">Theorem</span> <span class="id" type="var">preservation'</span> : <span style='font-size:120%;'>&forall;</span><span class="id" type="var">t</span> <span class="id" type="var">t'</span> <span class="id" type="var">T</span>,<br/>
&nbsp;&nbsp;&#x22A2; <span class="id" type="var">t</span> &#x2208; <span class="id" type="var">T</span> →<br/>
&nbsp;&nbsp;<span class="id" type="var">t</span> <span class="nowrap"><span style='font-size:85%;'><span style='vertical-align:6%;'><span style='letter-spacing:-.2em;'>-</span><span style='letter-spacing:-.2em;'>-</span></span>&gt;</span></span> <span class="id" type="var">t'</span> →<br/>
&nbsp;&nbsp;&#x22A2; <span class="id" type="var">t'</span> &#x2208; <span class="id" type="var">T</span>.<br/>
<span class="id" type="keyword">Proof</span> <span class="id" type="keyword">with</span> <span class="id" type="tactic">eauto</span>.<br/>
&nbsp;&nbsp;<span class="comment">(*&nbsp;请在此处解答&nbsp;*)</span> <span class="id" type="var">Admitted</span>.<br/>
</div>

<span class="proofbox">&#9744;</span> 
<div class="doc less-space">
<div class="paragraph"> </div>

 保型性定理也经常被称作<b>主语归约（subject reduction）</b>，因为它告诉了
    我们当类型关系的主语被归约时会发生什么。这一属于来自于把类型陈述想象为一句话，
    其中项是主语，类型是谓语。 
</div>

<div class="doc">
<a name="lab191"></a><h2 class="section">类型可靠性</h2>

<div class="paragraph"> </div>

 把可进行与保型性放在一起，我们可以看到一个良型的项永远不会有卡住状态。
</div>
<div class="code code-tight">

<span class="id" type="keyword">Definition</span> <span class="id" type="var">multistep</span> := (<span class="id" type="var">multi</span> <span class="id" type="var">step</span>).<br/>
<span class="id" type="keyword">Notation</span> "t<sub>1</sub> '<span class="nowrap"><span style='font-size:85%;'><span style='vertical-align:6%;'><span style='letter-spacing:-.2em;'>-</span><span style='letter-spacing:-.2em;'>-</span></span><span style='letter-spacing:-.2em;'>&gt;</span><span style='vertical-align:15%;'>*</span></span></span>' t<sub>2</sub>" := (<span class="id" type="var">multistep</span> <span class="id" type="var">t<sub>1</sub></span> <span class="id" type="var">t<sub>2</sub></span>) (<span class="id" type="tactic">at</span> <span class="id" type="var">level</span> 40).<br/><hr class='doublespaceincode'/>
<span class="id" type="keyword">Corollary</span> <span class="id" type="var">soundness</span> : <span style='font-size:120%;'>&forall;</span><span class="id" type="var">t</span> <span class="id" type="var">t'</span> <span class="id" type="var">T</span>,<br/>
&nbsp;&nbsp;&#x22A2; <span class="id" type="var">t</span> &#x2208; <span class="id" type="var">T</span> →<br/>
&nbsp;&nbsp;<span class="id" type="var">t</span> <span class="nowrap"><span style='font-size:85%;'><span style='vertical-align:6%;'><span style='letter-spacing:-.2em;'>-</span><span style='letter-spacing:-.2em;'>-</span></span><span style='letter-spacing:-.2em;'>&gt;</span><span style='vertical-align:15%;'>*</span></span></span> <span class="id" type="var">t'</span> →<br/>
&nbsp;&nbsp;~(<span class="id" type="var">stuck</span> <span class="id" type="var">t'</span>).<br/>
<div class="togglescript" id="proofcontrol7" onclick="toggleDisplay('proof7');toggleDisplay('proofcontrol7')"><span class="show"></span></div>
<div class="proofscript" id="proof7" onclick="toggleDisplay('proof7');toggleDisplay('proofcontrol7')">
<span class="id" type="keyword">Proof</span>.<br/>
&nbsp;&nbsp;<span class="id" type="tactic">intros</span> <span class="id" type="var">t</span> <span class="id" type="var">t'</span> <span class="id" type="var">T</span> <span class="id" type="var">HT</span> <span class="id" type="var">P</span>. <span class="id" type="tactic">induction</span> <span class="id" type="var">P</span>; <span class="id" type="tactic">intros</span> [<span class="id" type="var">R</span> <span class="id" type="var">S</span>].<br/>
&nbsp;&nbsp;<span class="id" type="tactic">destruct</span> (<span class="id" type="tactic">progress</span> <span class="id" type="var">x</span> <span class="id" type="var">T</span> <span class="id" type="var">HT</span>); <span class="id" type="tactic">auto</span>.<br/>
&nbsp;&nbsp;<span class="id" type="tactic">apply</span> <span class="id" type="var">IHP</span>. <span class="id" type="tactic">apply</span> (<span class="id" type="var">preservation</span> <span class="id" type="var">x</span> <span class="id" type="var">y</span> <span class="id" type="var">T</span> <span class="id" type="var">HT</span> <span class="id" type="var">H</span>).<br/>
&nbsp;&nbsp;<span class="id" type="tactic">unfold</span> <span class="id" type="var">stuck</span>. <span class="id" type="tactic">split</span>; <span class="id" type="tactic">auto</span>. <span class="id" type="keyword">Qed</span>.<br/>
</div>
</div>

<div class="doc">
<a name="lab192"></a><h2 class="section">额外练习</h2>

<div class="paragraph"> </div>

<a name="lab193"></a><h4 class="section">练习：2 星, standard, recommended (subject_expansion)</h4>
 在学习了主语归约属性后，你可能会好奇其相反的属性——主语<b>扩张</b>（subject expasion）
    ——是否也成立。也即，如果有 <span class="inlinecode"><span class="id" type="var">t</span></span> <span class="inlinecode"><span class="nowrap"><span style='font-size:85%;'><span style='vertical-align:6%;'><span style='letter-spacing:-.2em;'>-</span><span style='letter-spacing:-.2em;'>-</span></span>&gt;</span></span></span> <span class="inlinecode"><span class="id" type="var">t'</span></span> 且 <span class="inlinecode">&#x22A2;</span> <span class="inlinecode"><span class="id" type="var">t'</span></span> <span class="inlinecode">&#x2208;</span> <span class="inlinecode"><span class="id" type="var">T</span></span>，是否总是有
    <span class="inlinecode">&#x22A2;</span> <span class="inlinecode"><span class="id" type="var">t</span></span> <span class="inlinecode">&#x2208;</span> <span class="inlinecode"><span class="id" type="var">T</span></span>？如果是的话，请证明它。如果不是的话，请给出一个反例。
    （你并不需要在 Coq 中证明你的反例，不过也可以这样做。）

<div class="paragraph"> </div>

    <span class="comment">(*&nbsp;请在此处解答&nbsp;*)</span><br/>

</div>
<div class="code code-tight">
<span class="comment">(*&nbsp;请勿修改下面这一行：&nbsp;*)</span><br/>
<span class="id" type="keyword">Definition</span> <span class="id" type="var">manual_grade_for_subject_expansion</span> : <span class="id" type="var">option</span> (<span class="id" type="var">nat</span>*<span class="id" type="var">string</span>) := <span class="id" type="var">None</span>.<br/>
</div>

<span class="proofbox">&#9744;</span> 
<div class="doc less-space">
<div class="paragraph"> </div>

<a name="lab194"></a><h4 class="section">练习：2 星, standard (variation1)</h4>
 假设我们为类型关系添加新的规则：

<div class="paragraph"> </div>

<div class="code code-tight">
&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;|&nbsp;<span class="id" type="var">T_SccBool</span>&nbsp;:&nbsp;<span style='font-size:120%;'>&forall;</span><span class="id" type="var">t</span>,<br/>
&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&#x22A2;&nbsp;<span class="id" type="var">t</span>&nbsp;&#x2208;&nbsp;<span class="id" type="var">Bool</span>&nbsp;→<br/>
&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&#x22A2;&nbsp;<span class="id" type="var">scc</span>&nbsp;<span class="id" type="var">t</span>&nbsp;&#x2208;&nbsp;<span class="id" type="var">Bool</span>
<div class="paragraph"> </div>

</div>
  下面的哪些性质仍然成立？对于每个性质，写下“仍然成立”或“不成立”。
  如果性质不再成立，请给出一个反例。

<div class="paragraph"> </div>

<ul class="doclist">
<li> <span class="inlinecode"><span class="id" type="var">step</span></span> 的确定性
            <span class="comment">(*&nbsp;请在此处解答&nbsp;*)</span><br/>

</li>
<li> 可进性
            <span class="comment">(*&nbsp;请在此处解答&nbsp;*)</span><br/>

</li>
<li> 保型性
            <span class="comment">(*&nbsp;请在此处解答&nbsp;*)</span><br/>

</li>
</ul>

</div>
<div class="code code-tight">
<span class="comment">(*&nbsp;请勿修改下面这一行：&nbsp;*)</span><br/>
<span class="id" type="keyword">Definition</span> <span class="id" type="var">manual_grade_for_variation1</span> : <span class="id" type="var">option</span> (<span class="id" type="var">nat</span>*<span class="id" type="var">string</span>) := <span class="id" type="var">None</span>.<br/>
</div>

<span class="proofbox">&#9744;</span> 
<div class="doc less-space">
<div class="paragraph"> </div>

<a name="lab195"></a><h4 class="section">练习：2 星, standard (variation2)</h4>
 假设，我们仅为 <span class="inlinecode"><span class="id" type="var">step</span></span> 关系添加新的规则：

<div class="paragraph"> </div>

<div class="code code-tight">
&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;|&nbsp;<span class="id" type="var">ST_Funny1</span>&nbsp;:&nbsp;<span style='font-size:120%;'>&forall;</span><span class="id" type="var">t<sub>2</sub></span>&nbsp;<span class="id" type="var">t<sub>3</sub></span>,<br/>
&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;(<span class="id" type="var">test</span>&nbsp;<span class="id" type="var">tru</span>&nbsp;<span class="id" type="var">t<sub>2</sub></span>&nbsp;<span class="id" type="var">t<sub>3</sub></span>)&nbsp;<span class="nowrap"><span style='font-size:85%;'><span style='vertical-align:6%;'><span style='letter-spacing:-.2em;'>-</span><span style='letter-spacing:-.2em;'>-</span></span>&gt;</span></span>&nbsp;<span class="id" type="var">t<sub>3</sub></span>
<div class="paragraph"> </div>

</div>
   上面的哪些性质不再成立？对于不再成立的性质，给出一个反例。
            <span class="comment">(*&nbsp;请在此处解答&nbsp;*)</span><br/>

</div>
<div class="code code-tight">
<span class="comment">(*&nbsp;请勿修改下面这一行：&nbsp;*)</span><br/>
<span class="id" type="keyword">Definition</span> <span class="id" type="var">manual_grade_for_variation2</span> : <span class="id" type="var">option</span> (<span class="id" type="var">nat</span>*<span class="id" type="var">string</span>) := <span class="id" type="var">None</span>.<br/>
</div>

<span class="proofbox">&#9744;</span> 
<div class="doc less-space">
<div class="paragraph"> </div>

<a name="lab196"></a><h4 class="section">练习：2 星, standard, optional (variation3)</h4>
 假设，我们仅添加新的规则：

<div class="paragraph"> </div>

<div class="code code-tight">
&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;|&nbsp;<span class="id" type="var">ST_Funny2</span>&nbsp;:&nbsp;<span style='font-size:120%;'>&forall;</span><span class="id" type="var">t<sub>1</sub></span>&nbsp;<span class="id" type="var">t<sub>2</sub></span>&nbsp;<span class="id" type="var">t<sub>2</sub>'</span>&nbsp;<span class="id" type="var">t<sub>3</sub></span>,<br/>
&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;<span class="id" type="var">t<sub>2</sub></span>&nbsp;<span class="nowrap"><span style='font-size:85%;'><span style='vertical-align:6%;'><span style='letter-spacing:-.2em;'>-</span><span style='letter-spacing:-.2em;'>-</span></span>&gt;</span></span>&nbsp;<span class="id" type="var">t<sub>2</sub>'</span>&nbsp;→<br/>
&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;(<span class="id" type="var">test</span>&nbsp;<span class="id" type="var">t<sub>1</sub></span>&nbsp;<span class="id" type="var">t<sub>2</sub></span>&nbsp;<span class="id" type="var">t<sub>3</sub></span>)&nbsp;<span class="nowrap"><span style='font-size:85%;'><span style='vertical-align:6%;'><span style='letter-spacing:-.2em;'>-</span><span style='letter-spacing:-.2em;'>-</span></span>&gt;</span></span>&nbsp;(<span class="id" type="var">test</span>&nbsp;<span class="id" type="var">t<sub>1</sub></span>&nbsp;<span class="id" type="var">t<sub>2</sub>'</span>&nbsp;<span class="id" type="var">t<sub>3</sub></span>)
<div class="paragraph"> </div>

</div>
   this rule?  For each one that does, give a counter-example.
            <span class="comment">(*&nbsp;请在此处解答&nbsp;*)</span><br/>
 <span class="proofbox">&#9744;</span> 
<div class="paragraph"> </div>

<a name="lab197"></a><h4 class="section">练习：2 星, standard, optional (variation4)</h4>
 假设，我们仅添加新的规则：

<div class="paragraph"> </div>

<div class="code code-tight">
&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;|&nbsp;<span class="id" type="var">ST_Funny3</span>&nbsp;:<br/>
&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;(<span class="id" type="var">prd</span>&nbsp;<span class="id" type="var">fls</span>)&nbsp;<span class="nowrap"><span style='font-size:85%;'><span style='vertical-align:6%;'><span style='letter-spacing:-.2em;'>-</span><span style='letter-spacing:-.2em;'>-</span></span>&gt;</span></span>&nbsp;(<span class="id" type="var">prd</span>&nbsp;(<span class="id" type="var">prd</span>&nbsp;<span class="id" type="var">fls</span>))
<div class="paragraph"> </div>

</div>
   上面的哪些性质不再成立？对于不再成立的性质，给出一个反例。
<span class="comment">(*&nbsp;请在此处解答&nbsp;*)</span><br/>
 <span class="proofbox">&#9744;</span> 
<div class="paragraph"> </div>

<a name="lab198"></a><h4 class="section">练习：2 星, standard, optional (variation5)</h4>
 假设，我们仅添加新的规则：

<div class="paragraph"> </div>

<div class="code code-tight">
&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;|&nbsp;<span class="id" type="var">T_Funny4</span>&nbsp;:<br/>
&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&#x22A2;&nbsp;<span class="id" type="var">zro</span>&nbsp;&#x2208;&nbsp;<span class="id" type="var">Bool</span>
<div class="paragraph"> </div>

</div>
   上面的哪些性质不再成立？对于不再成立的性质，给出一个反例。
<span class="comment">(*&nbsp;请在此处解答&nbsp;*)</span><br/>
 <span class="proofbox">&#9744;</span> 
<div class="paragraph"> </div>

<a name="lab199"></a><h4 class="section">练习：2 星, standard, optional (variation6)</h4>
 假设，我们仅添加新的规则：

<div class="paragraph"> </div>

<div class="code code-tight">
&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;|&nbsp;<span class="id" type="var">T_Funny5</span>&nbsp;:<br/>
&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&#x22A2;&nbsp;<span class="id" type="var">prd</span>&nbsp;<span class="id" type="var">zro</span>&nbsp;&#x2208;&nbsp;<span class="id" type="var">Bool</span>
<div class="paragraph"> </div>

</div>
   上面的哪些性质不再成立？对于不再成立的性质，给出一个反例。
<span class="comment">(*&nbsp;请在此处解答&nbsp;*)</span><br/>
 <span class="proofbox">&#9744;</span> 
<div class="paragraph"> </div>

<a name="lab200"></a><h4 class="section">练习：3 星, standard, optional (more_variations)</h4>
 请使用上面的模式编写更多的练习。尝试有选择地使某些性质不再成立——
    即，对定义的改变只会导致某一个性质不再成立，而其他仍然成立。

</div>
<div class="code code-tight">
<span class="comment">(*&nbsp;请在此处解答&nbsp;*)</span><br/>
</div>

<span class="proofbox">&#9744;</span> 
<div class="doc less-space">
<div class="paragraph"> </div>

<a name="lab201"></a><h4 class="section">练习：1 星, standard (remove_prdzro)</h4>
 归约规则 <span class="inlinecode"><span class="id" type="var">ST_PrdZro</span></span> 可能有一点反直觉：我们想要让 <span class="inlinecode"></span> <span class="inlinecode"><span class="id" type="var">zro</span></span> 的前趋变为未定义的，
    而非定义为 <span class="inlinecode"><span class="id" type="var">zro</span></span>。我们是否可以通过仅仅移除 <span class="inlinecode"><span class="id" type="var">step</span></span> 中的某条规则达到这一点？
    这样做会导致别的问题出现吗？

<div class="paragraph"> </div>

<span class="comment">(*&nbsp;请在此处解答&nbsp;*)</span><br/>

</div>
<div class="code code-tight">
<span class="comment">(*&nbsp;请勿修改下面这一行：&nbsp;*)</span><br/>
<span class="id" type="keyword">Definition</span> <span class="id" type="var">manual_grade_for_remove_predzro</span> : <span class="id" type="var">option</span> (<span class="id" type="var">nat</span>*<span class="id" type="var">string</span>) := <span class="id" type="var">None</span>.<br/>
</div>

<span class="proofbox">&#9744;</span> 
<div class="doc less-space">
<div class="paragraph"> </div>

<a name="lab202"></a><h4 class="section">练习：4 星, advanced (prog_pres_bigstep)</h4>
 假设我们的求值关系是以大步语义方式定义的。请陈述类似的可进性和保型性定理。
    （你不需要证明他们。）

<div class="paragraph"> </div>

    你可以发现这两个属性中存在的局限吗？他们是否允许非停机的命令？我们为什么倾向于
    使用小步语义来陈述保型性和可进性？

<div class="paragraph"> </div>

<span class="comment">(*&nbsp;请在此处解答&nbsp;*)</span><br/>

</div>
<div class="code code-tight">
<span class="comment">(*&nbsp;请勿修改下面这一行：&nbsp;*)</span><br/>
<span class="id" type="keyword">Definition</span> <span class="id" type="var">manual_grade_for_prog_pres_bigstep</span> : <span class="id" type="var">option</span> (<span class="id" type="var">nat</span>*<span class="id" type="var">string</span>) := <span class="id" type="var">None</span>.<br/>
</div>

<span class="proofbox">&#9744;</span> 
<div class="code code-tight">

<span class="comment">(*&nbsp;Mon&nbsp;Oct&nbsp;28&nbsp;08:15:18&nbsp;UTC&nbsp;2019&nbsp;*)</span><br/>
</div>
</div>



</div>

</body>
</html>